From stdpp Require Import prelude finite.
From Coq Require Import FinFun FunctionalExtensionality Program.
From VLSM Require Import Lib.Preamble Lib.ListExtras Lib.StdppListSet Lib.FinExtras.
From VLSM Require Import Core.VLSM Core.VLSMProjections Core.Composition Core.ProjectionTraces.
From VLSM Require Import Core.SubProjectionTraces Core.Equivocation Core.Equivocation.NoEquivocation.
From VLSM Require Import Core.Equivocators.Common Core.Equivocators.Projections.
From VLSM Require Import Core.Equivocators.MessageProperties.
From VLSM Require Import Core.Equivocators.Composition.Common.

Section equivocators_composition_projections.

Context {message : Type}
  `{finite.Finite index}
  (IM : index -> VLSM message)
  `{forall i : index, HasBeenSentCapability (IM i)}
  (equivocator_descriptors := equivocator_descriptors IM)
  (equivocators_no_equivocations_vlsm := equivocators_no_equivocations_vlsm IM)
  (equivocators_state_project := equivocators_state_project IM)
  (equivocator_IM := equivocator_IM IM)
  (equivocator_descriptors_update := equivocator_descriptors_update IM)
  (proper_equivocator_descriptors := proper_equivocator_descriptors IM)
  (FreeE := free_composite_vlsm equivocator_IM)
  (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE)
  (Free := free_composite_vlsm IM)
  (PreFree := pre_loaded_with_all_messages_vlsm Free)
  .

Definition equivocators_transition_item_project
  (eqv_descriptors : equivocator_descriptors)
  (item : composite_transition_item equivocator_IM)
  : option (option (composite_transition_item IM) * equivocator_descriptors)
  :=
  let sx := equivocators_state_project eqv_descriptors (destination item) in
  let eqv := projT1 (l item) in
  let deqv := eqv_descriptors eqv in
  match
    equivocator_vlsm_transition_item_project
      (IM eqv)
      (composite_transition_item_projection equivocator_IM item)
      deqv
      with
  | Some (Some item', deqv') =>
    Some
      (Some (@Build_transition_item message (@type message Free)
        (existT eqv (l item'))
        (input item) sx (output item))
      , equivocator_descriptors_update eqv_descriptors eqv deqv')
  | Some (None, deqv') => Some (None, equivocator_descriptors_update eqv_descriptors eqv deqv')
  | None => None
  end.

Lemma equivocators_transition_item_project_preserves_equivocating_indices
  (descriptors : equivocator_descriptors)
  (item : composite_transition_item equivocator_IM)
  oitem idescriptors
  s
  (Hdescriptors : proper_equivocator_descriptors descriptors (destination item))
  (Ht : composite_transition equivocator_IM (l item) (s, input item) = (destination item, output item))
  (Hv : composite_valid equivocator_IM (l item) (s, input item))
  (Hpr : equivocators_transition_item_project descriptors item = Some (oitem, idescriptors))
  :
    (set_union (equivocating_indices IM (enum index) s) (newmachine_descriptors_list IM (enum index) idescriptors)) ⊆
    (set_union (equivocating_indices IM (enum index) (destination item)) (newmachine_descriptors_list IM (enum index) descriptors)).
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
item: composite_transition_item equivocator_IM
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors 
  (destination item)
Ht: composite_transition equivocator_IM 
  (l item) 
  (s, input item) =
(destination item, output item)
Hv: composite_valid equivocator_IM 
  (l item) 
  (s, input item)
Hpr: equivocators_transition_item_project descriptors
  item = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (destination item))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
Proof.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
item: composite_transition_item equivocator_IM
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors 
  (destination item)
Ht: composite_transition equivocator_IM 
  (l item) 
  (s, input item) =
(destination item, output item)
Hv: composite_valid equivocator_IM 
  (l item) 
  (s, input item)
Hpr: equivocators_transition_item_project descriptors
  item = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (destination item))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  unfold equivocators_transition_item_project
    , composite_transition_item_projection
    , composite_transition_item_projection_from_eq  in Hpr; simpl in Hpr.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
item: composite_transition_item equivocator_IM
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors 
  (destination item)
Ht: composite_transition equivocator_IM 
  (l item) 
  (s, input item) =
(destination item, output item)
Hv: composite_valid equivocator_IM 
  (l item) 
  (s, input item)
Hpr: match
  equivocator_vlsm_transition_item_project
    (IM (projT1 (l item)))
    {|
      l :=
        eq_rect_r
         (λ n : index, vlabel (equivocator_IM n))
         (projT2 (l item)) eq_refl;
      input := input item;
      destination :=
        destination item (projT1 (l item));
      output := output item
    |} (descriptors (projT1 (l item)))
with
| Some (Some item', deqv') =>
    Some
      (Some
         {|
         l := existT (projT1 (l item)) (l item');
         input := input item;
         destination :=
         equivocators_state_project descriptors
         (destination item);
         output := output item
         |},
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
| Some (None, deqv') =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
| None => None
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (destination item))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  unfold eq_rect_r, eq_rect in Hpr; simpl in Hpr.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
item: composite_transition_item equivocator_IM
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors 
  (destination item)
Ht: composite_transition equivocator_IM 
  (l item) 
  (s, input item) =
(destination item, output item)
Hv: composite_valid equivocator_IM 
  (l item) 
  (s, input item)
Hpr: match
  equivocator_vlsm_transition_item_project
    (IM (projT1 (l item)))
    {|
      l := projT2 (l item);
      input := input item;
      destination :=
        destination item (projT1 (l item));
      output := output item
    |} (descriptors (projT1 (l item)))
with
| Some (Some item', deqv') =>
    Some
      (Some
         {|
         l := existT (projT1 (l item)) (l item');
         input := input item;
         destination :=
         equivocators_state_project descriptors
         (destination item);
         output := output item
         |},
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
| Some (None, deqv') =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
| None => None
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (destination item))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  match type of Hpr with
    (match ?exp with _ => _ end = _)
    => destruct exp as [(oitemx, deqv')|] eqn:Hitem_pr;[|congruence]
  end.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
item: composite_transition_item equivocator_IM
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors 
  (destination item)
Ht: composite_transition equivocator_IM 
  (l item) 
  (s, input item) =
(destination item, output item)
Hv: composite_valid equivocator_IM 
  (l item) 
  (s, input item)
oitemx: option
  (vtransition_item (IM (projT1 (l item))))
deqv': MachineDescriptor (IM (projT1 (l item)))
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM (projT1 (l item)))
  {|
    l := projT2 (l item);
    input := input item;
    destination :=
      destination item (projT1 (l item));
    output := output item
  |} (descriptors (projT1 (l item))) =
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT (projT1 (l item)) (l item');
         input := input item;
         destination :=
         equivocators_state_project descriptors
         (destination item);
         output := output item
         |},
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (destination item))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  simpl in Ht.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
item: composite_transition_item equivocator_IM
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors 
  (destination item)
Ht: (let (i, li) := l item in
 let (si', om') :=
   vtransition 
     (equivocator_IM i) li 
     (s i, input item) in
 (state_update equivocator_IM s i si', om')) =
(destination item, output item)
Hv: composite_valid equivocator_IM 
  (l item) 
  (s, input item)
oitemx: option
  (vtransition_item (IM (projT1 (l item))))
deqv': MachineDescriptor (IM (projT1 (l item)))
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM (projT1 (l item)))
  {|
    l := projT2 (l item);
    input := input item;
    destination :=
      destination item (projT1 (l item));
    output := output item
  |} (descriptors (projT1 (l item))) =
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT (projT1 (l item)) (l item');
         input := input item;
         destination :=
         equivocators_state_project descriptors
         (destination item);
         output := output item
         |},
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1 (l item)) deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (destination item))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  destruct item.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
l: label
input: option message
destination: state
output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (VLSM.destination
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |})
Ht: (let (i, li) :=
   VLSM.l
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |} in
 let (si', om') :=
   vtransition 
     (equivocator_IM i) li
     (s i,
     VLSM.input
       {|
         l := l;
         input := input;
         destination := destination;
         output := output
       |}) in
 (state_update equivocator_IM s i si', om')) =
(VLSM.destination
   {|
     l := l;
     input := input;
     destination := destination;
     output := output
   |},
VLSM.output
  {|
    l := l;
    input := input;
    destination := destination;
    output := output
  |})
Hv: composite_valid equivocator_IM
  (VLSM.l
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |})
  (s,
  VLSM.input
    {|
      l := l;
      input := input;
      destination := destination;
      output := output
    |})
oitemx: option
  (vtransition_item
     (IM
        (projT1
         (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |}))))
deqv': MachineDescriptor
  (IM
     (projT1
        (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |})))
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM
     (projT1
        (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |})))
  {|
    l :=
      projT2
        (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |});
    input :=
      VLSM.input
        {|
         l := l;
         input := input;
         destination := destination;
         output := output
        |};
    destination :=
      VLSM.destination
        {|
         l := l;
         input := input;
         destination := destination;
         output := output
        |}
        (projT1
         (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |}));
    output :=
      VLSM.output
        {|
         l := l;
         input := input;
         destination := destination;
         output := output
        |}
  |}
  (descriptors
     (projT1
        (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |}))) = 
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l :=
         existT
         (projT1
         (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |})) 
         (VLSM.l item');
         input :=
         VLSM.input
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |};
         destination :=
         equivocators_state_project descriptors
         (VLSM.destination
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |});
         output :=
         VLSM.output
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |}
         |},
      equivocator_descriptors_update descriptors
        (projT1
         (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |})) deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1
         (VLSM.l
         {|
         l := l;
         input := input;
         destination := destination;
         output := output
         |})) deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (VLSM.destination
          {|
            l := l;
            input := input;
            destination := destination;
            output := output
          |}))
    (newmachine_descriptors_list IM (enum index)
       descriptors) simpl in *.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
l: _composite_label equivocator_IM
input: option message
destination: _composite_state equivocator_IM
output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors destination
Ht: (let (i, li) := l in
 let (si', om') :=
   vtransition (equivocator_IM i) li (s i, input) in
 (state_update equivocator_IM s i si', om')) =
(destination, output)
Hv: let (i, li) := l in
vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM (projT1 l)))
deqv': MachineDescriptor (IM (projT1 l))
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM (projT1 l))
  {|
    l := projT2 l;
    input := input;
    destination := destination (projT1 l);
    output := output
  |} (descriptors (projT1 l)) =
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT (projT1 l) (VLSM.l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         destination;
         output := output
         |},
      equivocator_descriptors_update descriptors
        (projT1 l) deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1 l) deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index) destination)
    (newmachine_descriptors_list IM (enum index)
       descriptors) destruct l as (i, li).
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input: option message
destination: _composite_state equivocator_IM
output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors destination
Ht: (let (si', om') :=
   vtransition (equivocator_IM i) li (s i, input) in
 (state_update equivocator_IM s i si', om')) =
(destination, output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option
  (vtransition_item
     (IM (projT1 (existT i li))))
deqv': MachineDescriptor (IM (projT1 (existT i li)))
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM (projT1 (existT i li)))
  {|
    l := projT2 (existT i li);
    input := input;
    destination :=
      destination (projT1 (existT i li));
    output := output
  |} (descriptors (projT1 (existT i li))) =
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l :=
         existT (projT1 (existT i li)) (l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         destination;
         output := output
         |},
      equivocator_descriptors_update descriptors
        (projT1 (existT i li)) deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        (projT1 (existT i li)) deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index) destination)
    (newmachine_descriptors_list IM (enum index)
       descriptors) simpl in *.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input: option message
destination: _composite_state equivocator_IM
output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors destination
Ht: (let (si', om') :=
   vtransition (equivocator_IM i) li (s i, input) in
 (state_update equivocator_IM s i si', om')) =
(destination, output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination := destination i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT i (l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         destination;
         output := output
         |},
      equivocator_descriptors_update descriptors
        i deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        i deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index) destination)
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  destruct (vtransition (equivocator_IM i) li (s i, input))
    as (si', om') eqn:Htei.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input: option message
destination: _composite_state equivocator_IM
output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors destination
si': state
om': option message
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', om')
Ht: (state_update equivocator_IM s i si', om') =
(destination, output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination := destination i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT i (l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         destination;
         output := output
         |},
      equivocator_descriptors_update descriptors
        i deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        i deqv')
end = Some (oitem, idescriptors)
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index) destination)
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  inversion Ht.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input: option message
destination: _composite_state equivocator_IM
output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
Hdescriptors: proper_equivocator_descriptors
  descriptors destination
si': state
om': option message
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', om')
Ht: (state_update equivocator_IM s i si', om') =
(destination, output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination := destination i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT i (l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         destination;
         output := output
         |},
      equivocator_descriptors_update descriptors
        i deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        i deqv')
end = Some (oitem, idescriptors)
H2: state_update equivocator_IM s i si' = destination
H3: om' = output
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (state_update equivocator_IM s i si'))
    (newmachine_descriptors_list IM (enum index)
       descriptors) subst.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Ht: (state_update equivocator_IM s i si', output) =
(state_update equivocator_IM s i si', output)
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT i (l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         (state_update equivocator_IM s i si');
         output := output
         |},
      equivocator_descriptors_update descriptors
        i deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        i deqv')
end = Some (oitem, idescriptors)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (state_update equivocator_IM s i si'))
    (newmachine_descriptors_list IM (enum index)
       descriptors) clear Ht.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
oitem: option (composite_transition_item IM)
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hpr: match oitemx with
| Some item' =>
    Some
      (Some
         {|
         l := existT i (l item');
         input := input;
         destination :=
         equivocators_state_project descriptors
         (state_update equivocator_IM s i si');
         output := output
         |},
      equivocator_descriptors_update descriptors
        i deqv')
| None =>
    Some
      (None,
      equivocator_descriptors_update descriptors
        i deqv')
end = Some (oitem, idescriptors)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     idescriptors)
⊆ set_union
    (equivocating_indices IM (enum index)
       (state_update equivocator_IM s i si'))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  replace idescriptors with (equivocator_descriptors_update descriptors i deqv')
    by (destruct oitemx;congruence);clear oitem Hpr.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
set_union (equivocating_indices IM (enum index) s)
  (newmachine_descriptors_list IM (enum index)
     (equivocator_descriptors_update descriptors i
        deqv'))
⊆ set_union
    (equivocating_indices IM (enum index)
       (state_update equivocator_IM s i si'))
    (newmachine_descriptors_list IM (enum index)
       descriptors)
  intros eqv Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv
∈ set_union
    (equivocating_indices IM (enum index) s)
    (newmachine_descriptors_list IM
       (enum index)
       (equivocator_descriptors_update
         descriptors i deqv'))
eqv
∈ set_union
    (equivocating_indices IM (enum index)
       (state_update equivocator_IM s i si'))
    (newmachine_descriptors_list IM (enum index)
       descriptors) apply set_union_iff in Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors i deqv')
eqv
∈ set_union
    (equivocating_indices IM (enum index)
       (state_update equivocator_IM s i si'))
    (newmachine_descriptors_list IM (enum index)
       descriptors) apply set_union_iff.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors i deqv')
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors
  destruct (decide (eqv = i)).
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors i deqv')
e: eqv = i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors i deqv')
n: eqv ≠ i
eqv
∈ equivocating_indices IM 
    (enum index) 
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index) descriptors
  -
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors i deqv')
e: eqv = i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors subst i.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors eqv deqv')
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s eqv si'
        eqv;
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s eqv
     si')
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s eqv si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors
    unfold equivocating_indices in *.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: eqv
∈ filter
    (λ i : index,
       is_equivocating_state (IM i) (s i))
    (enum index)
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors eqv deqv')
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s eqv si'
        eqv;
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s eqv
     si')
eqv
∈ filter
    (λ i : index,
       is_equivocating_state (IM i)
         (state_update equivocator_IM s eqv si' i))
    (enum index)
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors
    unfold newmachine_descriptors_list in *.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: eqv
∈ filter
    (λ i : index,
       is_equivocating_state (IM i) (s i))
    (enum index)
∨ eqv
  ∈ filter
      (λ i : index,
         is_newmachine_descriptor 
         (IM i)
         (equivocator_descriptors_update
         descriptors eqv deqv' i)) 
      (enum index)
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s eqv si'
        eqv;
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s eqv
     si')
eqv
∈ filter
    (λ i : index,
       is_equivocating_state (IM i)
         (state_update equivocator_IM s eqv si' i))
    (enum index)
∨ eqv
  ∈ filter
      (λ i : index,
         is_newmachine_descriptor (IM i)
           (descriptors i)) (enum index)
    rewrite! elem_of_list_filter in *.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s eqv si'
        eqv;
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s eqv
     si')
is_equivocating_state (IM eqv)
  (state_update equivocator_IM s eqv si' eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
  ∧ eqv ∈ enum index
    rewrite state_update_eq.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s eqv si'
        eqv;
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s eqv
     si')
is_equivocating_state (IM eqv) si' ∧ eqv ∈ enum index
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
  ∧ eqv ∈ enum index
    specialize (Hdescriptors eqv).
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s eqv si'
        eqv;
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_descriptor 
  (IM eqv) 
  (descriptors eqv)
  (state_update equivocator_IM s eqv
     si' eqv)
is_equivocating_state (IM eqv) si' ∧ eqv ∈ enum index
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
  ∧ eqv ∈ enum index
    rewrite state_update_eq in Hitem_pr, Hdescriptors.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination := si';
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_descriptor 
  (IM eqv) 
  (descriptors eqv) si'
is_equivocating_state (IM eqv) si' ∧ eqv ∈ enum index
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
  ∧ eqv ∈ enum index
    cut (is_equivocating_state (IM eqv) si' \/  is_newmachine_descriptor (IM eqv) (descriptors eqv)).
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination := si';
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_descriptor 
  (IM eqv) 
  (descriptors eqv) si'
is_equivocating_state (IM eqv) si'
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
→ is_equivocating_state (IM eqv) si'
  ∧ eqv ∈ enum index
  ∨ is_newmachine_descriptor (IM eqv)
      (descriptors eqv) ∧ eqv ∈ enum index
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination := si';
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_descriptor 
  (IM eqv) 
  (descriptors eqv) si'
is_equivocating_state (IM eqv) si'
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
      by intuition.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination := si';
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_descriptor 
  (IM eqv) 
  (descriptors eqv) si'
is_equivocating_state (IM eqv) si'
∨ is_newmachine_descriptor (IM eqv) (descriptors eqv)
    apply
      (equivocator_transition_item_project_preserves_equivocating_indices (IM eqv) {|
      l := li;
      input := input;
      destination := si';
      output := output |} _ Hdescriptors _ _ Hitem_pr _ Hv Htei).
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
li: vlabel (equivocator_IM eqv)
input, output: option message
idescriptors: equivocator_descriptors
oitemx: option (vtransition_item (IM eqv))
si': state
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM eqv)
  {|
    l := li;
    input := input;
    destination := si';
    output := output
  |} (descriptors eqv) =
Some (oitemx, deqv')
Hv: vvalid (equivocator_IM eqv) li (s eqv, input)
Htei: vtransition 
  (equivocator_IM eqv) li 
  (s eqv, input) = 
(si', output)
Hdescriptors: proper_descriptor 
  (IM eqv) 
  (descriptors eqv) si'
is_equivocating_state (IM eqv) (s eqv)
∨ is_newmachine_descriptor (IM eqv) deqv'
    clear -Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors IM
→ ∀ i : index,
MachineDescriptor (IM i) → ∀ j : index, MachineDescriptor (IM j)
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (equivocator_descriptors_update descriptors
       eqv deqv' eqv) ∧ 
  eqv ∈ enum index
is_equivocating_state (IM eqv) (s eqv)
∨ is_newmachine_descriptor (IM eqv) deqv'
    unfold equivocator_descriptors_update in Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors IM
→ ∀ i : index,
MachineDescriptor (IM i) → ∀ j : index, MachineDescriptor (IM j)
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor 
    (IM eqv)
    (Common.equivocator_descriptors_update IM
       descriptors eqv deqv' eqv)
  ∧ eqv ∈ enum index
is_equivocating_state (IM eqv) (s eqv)
∨ is_newmachine_descriptor (IM eqv) deqv'
    rewrite equivocator_descriptors_update_eq in Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors IM
→ ∀ i : index,
MachineDescriptor (IM i) → ∀ j : index, MachineDescriptor (IM j)
descriptors: equivocator_descriptors
eqv: index
s: composite_state equivocator_IM
deqv': MachineDescriptor (IM eqv)
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
∨ is_newmachine_descriptor (IM eqv) deqv'
  ∧ eqv ∈ enum index
is_equivocating_state (IM eqv) (s eqv)
∨ is_newmachine_descriptor (IM eqv) deqv'
    intuition.
  -
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index)
      (equivocator_descriptors_update
         descriptors i deqv')
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors destruct Heqv as [Heqv | Heqv].
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv
∈ newmachine_descriptors_list IM 
    (enum index)
    (equivocator_descriptors_update descriptors
       i deqv')
n: eqv ≠ i
eqv
∈ equivocating_indices IM 
    (enum index) 
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM 
      (enum index) descriptors
    +
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors left.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv ∈ equivocating_indices IM (enum index) s
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
      apply elem_of_list_filter in Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_equivocating_state (IM eqv) (s eqv)
∧ eqv ∈ enum index
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
      destruct Heqv as [Heqv Hin].
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_equivocating_state (IM eqv) (s eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
      apply elem_of_list_filter.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_equivocating_state (IM eqv) (s eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_equivocating_state (IM eqv)
  (state_update equivocator_IM s i si' eqv)
∧ eqv ∈ enum index
      split; [|assumption].
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_equivocating_state (IM eqv) (s eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_equivocating_state (IM eqv)
  (state_update equivocator_IM s i si' eqv)
      rewrite state_update_neq by apply n.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_equivocating_state (IM eqv) (s eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_equivocating_state (IM eqv) (s eqv)
      assumption.
    +
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv
∈ newmachine_descriptors_list IM 
    (enum index)
    (equivocator_descriptors_update descriptors
       i deqv')
n: eqv ≠ i
eqv
∈ equivocating_indices IM (enum index)
    (state_update equivocator_IM s i si')
∨ eqv
  ∈ newmachine_descriptors_list IM (enum index)
      descriptors right.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: eqv
∈ newmachine_descriptors_list IM 
    (enum index)
    (equivocator_descriptors_update descriptors
       i deqv')
n: eqv ≠ i
eqv
∈ newmachine_descriptors_list IM (enum index)
    descriptors
      apply elem_of_list_filter in Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_newmachine_descriptor 
  (IM eqv)
  (equivocator_descriptors_update descriptors i
     deqv' eqv) ∧ 
eqv ∈ enum index
n: eqv ≠ i
eqv
∈ newmachine_descriptors_list IM (enum index)
    descriptors
      destruct Heqv as [Heqv Hin].
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_newmachine_descriptor 
  (IM eqv)
  (equivocator_descriptors_update descriptors i
     deqv' eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
eqv
∈ newmachine_descriptors_list IM (enum index)
    descriptors
      apply elem_of_list_filter.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_newmachine_descriptor 
  (IM eqv)
  (equivocator_descriptors_update descriptors i
     deqv' eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_newmachine_descriptor (IM eqv) (descriptors eqv)
∧ eqv ∈ enum index
      split; [|assumption].
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_newmachine_descriptor 
  (IM eqv)
  (equivocator_descriptors_update descriptors i
     deqv' eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_newmachine_descriptor (IM eqv) (descriptors eqv)
      unfold equivocator_descriptors_update in Heqv.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_newmachine_descriptor 
  (IM eqv)
  (Common.equivocator_descriptors_update IM
     descriptors i deqv' eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_newmachine_descriptor (IM eqv) (descriptors eqv)
      rewrite equivocator_descriptors_update_neq in Heqv by apply n.
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
equivocator_descriptors:= Common.equivocator_descriptors
  IM: Type
equivocators_no_equivocations_vlsm:= Common.equivocators_no_equivocations_vlsm
  IM: VLSM message
equivocators_state_project:= Common.equivocators_state_project
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM))
  → vstate
      (free_composite_vlsm
         IM)
equivocator_IM:= Common.equivocator_IM IM: index → VLSM message
equivocator_descriptors_update:= Common.equivocator_descriptors_update
  IM: Common.equivocator_descriptors
  IM
→ ∀ i : index,
    MachineDescriptor
      (IM i)
    → ∀ j : index,
        MachineDescriptor
         (IM j)
proper_equivocator_descriptors:= Common.proper_equivocator_descriptors
  IM: Common.equivocator_descriptors
  IM
→ vstate
    (free_composite_vlsm
       (Common.equivocator_IM
         IM)) → Prop
FreeE:= free_composite_vlsm equivocator_IM: VLSM message
PreFreeE:= pre_loaded_with_all_messages_vlsm FreeE: VLSM message
Free:= free_composite_vlsm IM: VLSM message
PreFree:= pre_loaded_with_all_messages_vlsm Free: VLSM message
descriptors: equivocator_descriptors
i: index
li: vlabel (equivocator_IM i)
input, output: option message
idescriptors: equivocator_descriptors
s: composite_state equivocator_IM
si': state
Hdescriptors: proper_equivocator_descriptors
  descriptors
  (state_update equivocator_IM s i si')
Htei: vtransition (equivocator_IM i) li (s i, input) =
(si', output)
Hv: vvalid (equivocator_IM i) li (s i, input)
oitemx: option (vtransition_item (IM i))
deqv': MachineDescriptor (IM i)
Hitem_pr: equivocator_vlsm_transition_item_project
  (IM i)
  {|
    l := li;
    input := input;
    destination :=
      state_update equivocator_IM s i si' i;
    output := output
  |} (descriptors i) = 
Some (oitemx, deqv')
eqv: index
Heqv: is_newmachine_descriptor 
  (IM eqv) 
  (descriptors eqv)
Hin: eqv ∈ enum index
n: eqv ≠ i
is_newmachine_descriptor (IM eqv) (descriptors eqv)
      assumption.
Qed.